product_perm_lems: THEORY
%------------------------------------------------------------------------------
%
% NOTE: At some point this theory should be integrated with
%       structures@permutation
%
%------------------------------------------------------------------------------

BEGIN


   IMPORTING reals@product_fseq_posnat
   IMPORTING structures@permutations_fseq[posnat,<=]
   IMPORTING structures@sort_fseq[posnat,<=]
  
   fs,fs1,fs2: VAR fseq[posnat]

   swap(fs)(i,j: nat): fseq[posnat] =
                      (# length := length(fs),
                         seq := (LAMBDA (ii: nat):
                                    IF ii >= length(fs) THEN default
                                    ELSIF    ii = i THEN fs(j)
                                    ELSIF ii = j THEN fs(i)
                                    ELSE fs(ii)
                                    ENDIF)
                      #)

   i,j,k,l: VAR nat
   swap_len: LEMMA length(swap(fs)(i,j)) = length(fs)

   swap_eq_arg: LEMMA swap(fs)(i,i) = fs

   swap_symm: LEMMA swap(fs)(i,j) = swap(fs)(j,i)


   prod_swap_prep: LEMMA i <= j AND (j < k OR i > l) IMPLIES
                       product(k, l, swap(fs)(i, j)`seq)
                       = product(k,l, fs`seq)

   prod_swap_prep2: LEMMA i <= j AND (i < k AND j > l) IMPLIES
                          product(k, l, swap(fs)(i, j)`seq) = product(k,l, fs`seq)

   product_swap: LEMMA FORALL (i,j: below(length(fs))):
                              product(swap(fs)(i,j)) = product(fs)


   swap_is_permutation: LEMMA FORALL (i,j: below(length(fs))):
                                   permutation?(swap(fs)(i,j),fs)


   product_permutation: LEMMA permutation?(fs1,fs2) IMPLIES
                              product(fs1) = product(fs2)


   non_decreasing?(fs): bool = 
       (FORALL (i,j: below(length(fs))): i < j IMPLIES seq(fs)(i) <= seq(fs)(j))


   length_sort: LEMMA (sort(fs))`length = fs`length



   product_sort: LEMMA product(sort(fs)) = product(fs)


END product_perm_lems